Formal Verification of Consensus Algorithms
See also Formal verification of cryptographic protocols for UC model, process calculous, etc.
Blockchain
Nakamoto consensus
ToyChain
Paper Mechanising Blockchain Consensus, GitHub Repo
George Pirlea, Ilya Sergey (University College London, UK)
Bitcoin-specific extention GitHub Repo
Towards Verified Blockchain Architectures: A Case Study on Interactive Architecture Verification
Based on FACTum, which is based on Isabelle/HOL
Hierarchical Specification and Verification of Architectural Design Patterns
GitHub
Difference with Toychain:
The proved property: blockchain integrity, i.e., that additions to the blockchain are guaranteed to be persistent.
Similar to common prefix
Consideration of attackers
Model Checking Bitcoin and other Proof-of-Work Consensus Protocols
Max DiGiacomo-Castillo, Yiyun Liang, Advay Pal, John C. Mitchell (Stanford)
UPPAAL-SMC
Analyzing Selfish mining
Ouroboros
Forkable Strings of ouroboros paper in Isabelle/HOL
bitbucket
Kawin Worrasangasilpa
Psi/Chi calculus, IOHK Blog post, GitHub
psi calculus: a generalization of the pi calculus with more advanced features
we can embed (shallow-embedding?) it as a domain-specific language (DSL) in Haskell and:
both execute and run (it’s just Haskell after all)
test using QuickCheck (Haskell’s randomized testing tool)
do formal verification using the psi calculus metatheory.
Proofs in Isabelle
Formalizing Nakamoto-Style Proof of Stake
Søren Eller Thomsen and Bas Spitters
Safety and Liveness of a protocol similat to Ouroboros Praos
GitHub
Casper FFG
Formal verification of Hybrid Casper FFG with Coq
Runtime Verification
GitHub Repo
Based on Toychain
Verification of previous version of Casper FFG with Isabelle by Yoichi Hirai
A repository for PoS related formal methods
Alloy, Isabelle
Slide, Article
Verifying Gasper with Dynamic Validator Sets in Coq
GitHub Blog
Runtime Verification
CBC Casper
See Casper CBC: Formal verification
Algorand
Towards a Verified Model of the Algorand Consensus Protocol in Coq
GitHub by Runtime Verification
Report
Stellar Consensus Protocol
Verification with Isabelle and Ivy
GitHub, Slide
Formalizes some definitions and proofs of the Stellar whitepaper and a simpler take on federated voting in Isabelle
Formalizes and proves safety of the ballot protocol in Ivy
Formal Modeling and Verification of a Federated Byzantine Agreement Algorithm for Blockchain Platforms
Junghun Yoo (University of Oxford) et al.
Stellar Consensus Protocol in UPPAAL
Certifying Blockchain Byzantine Fault Tolerance
Pierre Tholoniat (University of Sydney), Vincent Gramoli (University of Sydney)
Verify Two components of Red Belly Blockchain using the ByMC model checker
1. A simple broadcast primitive
2. A blockchain consensus algorithm written in 309
Others
Formal verification of fairness of the Tendermint proposer election algorithm
GitHub, Idris
Traditional BFT
Velisarios
Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq (2018)
ESOP'18
Vincent Rahli et al. (University of Luxembourg)
GitHub
A logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols
Extends the Logic of Events (LoE) in order to reason not only about crash faults, but also about arbitrary faults.
In LoE, an event is an abstract entity that corresponds either (1) to the handling of a received message, or (2) to some arbitrary activity about which no information is provided.
As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area’s reference protocol: PBFT. (See Velisarios/PBFT)
proved only safety
ref: a survey paper by the author An Ecosystem for Verifying Implementations of BFT protocols (Ivana Vukotic et.al)
https://gyazo.com/4d01242baf866458468d6f205f68e6b6
Others
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
Develop a methodology for deductive verification of thresholdbased distributed protocols using decidable logic
Decomposition into two well-established decidable logics
Implemented with Z3 and CVC4
Verified Byzantine one-step consensus, hybrid reliable broadcast and fast Byzantine Paxos
Traditional CFT
Verdi
A framework for formally verifying distributed systems implementations in Coq
Website, Slide (Japanese)
Paper Verdi: A Framework for Implementing and Formally Verifying Distributed Systems (2015)
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas Anderson (University of Washington, USA)
cited 118
GitHub: verdi slide
Contribution from Karl Palmskog
Verdi Raft
paper Planning for Change in a Formal Verification of the Raft Consensus Protocol
GitHub verdi-raft
proved only safety
Verdi currently supports verifying safety properties, but not liveness properties, and none of Verdi’s network semantics currently capture Byzantine fault models. We believe that Verdi could be extended to support these features: liveness properties could be verified by supporting infinite traces and adding fairness hypotheses as axioms as in TLA, while Byzantine fault models can be supported by adding more non-determinism in the network semantics.
Verdi Chord
GitHub verdi-chord
DISEL
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Programming and Proving with Distributed Protocols
Ilya Sergey (University College London, UK)
James R. Wilcox, Zachary Tatlock (University of Washington, USA)
Programming Language Abstractions for Modularly Verified Distributed Systems
GitHub Repo
Contribution from Karl Palmskog
Example of Two-phase commit
Ivy
See Ivy about the tool itself
Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
Multi-Paxos, Raft
Slide
Paxos Made EPR: Decidable Reasoning about Distributed Protocols
Deductive verification based on effectively propositional logic (EPR)
A decidable fragment of first-order logic (also known as the Bernays-Schönfinkel-Ramsey class).
The finite model property, allowing to display violations as finite structures which are intuitive for users.
Modeling protocols using general (uninterpreted) first-order logic, and then systematically transforming the model to obtain a model and an inductive invariant that are decidable to check.
The steps of the transformations are also mechanically checked, ensuring the soundness of the method
Paxos and its variants
Implemented in Ivy
EventML
Interfacing with Proof Assistants for Domain Specific Programming Using EventML (2012)
Vincent Rahli (Cornell University)
A language for implementing distributed systems
Developing Correctly Replicated Databases Using Formal Tools (2014)
Nicolas Schiper Vincent Rahli Robbert Van Renesse Mark Bickford Robert L. Constable (Cornell University)
from Verdi Raft's paper
EventML programs can be verified in NuPRL using the Logic of Events.
EventML and the Logic of Events have been used to verify an implementation of Multi-Paxos, a total-order broadcast service, used as part of a distributed database
IronFleet
IronFleet: Proving Practical Distributed Systems Correct (2015)
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, Brian Zill (Microsoft Research)
cited 134
GitHub /ironfleet
TLA-style state-machine refinement and Hoare-logic verification (Dafny, an SMT-based program verification toolchain)
from Verdi Raft's paper,
This approach enables building practical distributed systems and proving both safety and, unlike our Raft proof in Verdi, liveness properties.
Also unlike our Raft implementation in Verdi, IronFleet’s implementation of Paxos supports many important practical features including verified marshaling and parsing, state transfer, and log truncation
Head-Of model
The Heard-Of Model: Computing in Distributed Systems with Benign Failures
Bernadette Charron-Bost (Ecole polytechnique), Andr´e Schiper (EPFL)
Verifying Fault-Tolerant Distributed Algorithms In The Heard-Of Model
Henri Debrat (Universit´e de Lorraine & LORIA) and Stephan Merz (Inria Nancy Grand-Est & LORIA)
Formalize Heard-Of model in Isabelle/HOL the
HO model can represent algorithms that operate in communication-closed rounds, which is true of virtually all known fault-tolerant distributed algorithms.
Both safety and liveness
Tolerating Corrupted Communication
Extenstion for Byzantine faults
Martin Biely (TU Wien) et al.
PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms
GitHub
DSL based on Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages
Paxos
Does not deal with Byzantine faults
Consensus Refined
Ognjen Maric, Christoph Sprenger, and David Basin (ETH Zurich)
AFP
Cutoff Bounds for Consensus Algorithms
Ognjen Maric, Christoph Sprenger, and David Basin (ETH Zurich)
Define a language ConsL, capable of expressing numerous consensus algorithms (Paxos, Chandra-Toueg, Ben-Or etc.)
Leverage model checking to provide the first fully automated decision procedure applicable to a range of consensus algorithms (Promela/Spin)
Video
Other Isabelle/HOL works
Proving the Correctness of Disk Paxos in Isabelle/HOL
From TLA+ specification to Isabelle
AFP
Model checking of traditional protocols
TLA+
Two-phase commit Slide
Paxos
GitHub
Mechanically Checked Safety Proof of a Byzantine Paxos Algorithm
Leslie Lamport
SPIN
Paxos
Giorgio Delzanno et.al.
Model Checking Paxos in Spin
Model Checking Distributed Consensus
Raft (Japanese)
SMV
Randomised Consensus Protocol
Non-probabilistic Verification: the verification of Validity and Agreement and the non-probabilistic arguments for proving Probabilistic wait-free termination using Cadence SMV
Probabilistic Verification: the verification of the probabilistic arguments for proving Probabilistic wait-free termination using PRISM
Related/Others
Practical Byzantine Fault Tolerance (Ph.D thesis, 2001)
Miguel Castro (MIT)
Formal proof of safety and liveness of pBFT using I/O automata
Blockchain Abstract Data Type
Emmanuelle Anceaume (IRISA) et al.
Bitcoin, GHOST, Byzcoin, Algorand, PeerCensus, Red Belly
An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory
Yoichi Hirai
Slide
#Formal_verification #Coq #Isabelle